es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id} ).
e<e'.P(e)  (((first(e'))) c (P(pred(e'))  e<pred(e').P(e))) 

latex

Definitions	x:A. B(x), , P  Q, e<e'.P(e), x(s), A c B, A, P  Q, P & Q, P  Q, P  Q, t  T, x. t(x), x:A. B(x), (e <loc e')
Lemmas	existse-before wf, es-E wf, Id wf, es-loc wf, assert wf, false wf, es-loc-pred, event system wf, es-locl-iff, es-pred-locl, es-causl wf, es-locl transitivity2, es-le weakening, es-locl wf